\begin{tabbing}
trigger{-}send($A$;${\it ds}$;$x$;${\it cond}$;$l$;${\it tg}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Rsends(${\it ds}$;$x$;${\it cond}$.1;$l$;if isrcvl($l$;$x$)\+
\\[0ex]then ${\it tg}$ : $A$ $\oplus$ tag($x$) : ${\it cond}$.1
\\[0ex]else ${\it tg}$ : $A$
\\[0ex]fi ;[\=$<$${\it tg}$\+
\\[0ex], \=$\lambda$$s$,$v$. if can{-}apply($\lambda$$p$.let $s$,$v$ = $p$ in (${\it cond}$.2)($s$,$v$);$<$$s$, $v$$>$)\+
\\[0ex]then [do{-}apply($\lambda$$p$.let $s$,$v$ = $p$ in (${\it cond}$.2)($s$,$v$);$<$$s$, $v$$>$)]
\\[0ex]else []
\\[0ex]fi 
\-\\[0ex]$>$])
\-\-
\end{tabbing}